i:Id, k:Knd. (has-src(i;k))  ((isrcv(k)) c (source(lnk(k)) = i)) 

latex

Definitions	x:A. B(x), P  Q, A c B, P & Q, P  Q, P  Q, t  T, , b, isrcv(k), isl(x), tt, if b then t else f fi , True, lnk(k), outl(x), x. t(x), has-src(i;k), p  q, Knd, ff, False, x(s)
Lemmas	assert wf, has-src wf, isrcv wf, Id wf, lsrc wf, lnk wf, Knd wf, assert-eq-id, pi1 wf, IdLnk wf